open Sets
open Syntax

type intT = int * IntSet.t;;
type specT = SAFETY | GUARANTEE | OBLIGATION | REGULAR

let _ =
	let mode = ref "" in
	let input1 = ref "" in
	let input2 = ref "" in
 
	let usage = "usage: "^Sys.argv.(0)^" <option>" in
	let speclist = [
		("-nba2smv", Arg.String (fun s -> mode:="-nba2smv"; input1:=s), "<spec.spin> : outputs an nuSMV module of the first NBA");
		("-smv", Arg.Tuple [Arg.String (fun s -> mode:="-smv"; input1:=s); Arg.Set_string(input2)], "<spec_neg.spin> <spec.spin> : outputs an nuSMV module of the first NBA");
		("-spin", Arg.Tuple [Arg.String (fun s -> mode:="-spin"; input1:=s); Arg.Set_string(input2)], "<spec_neg.spin> <spec.spin> : outputs a SPIN module of the first NBA");
		("-dot", Arg.Tuple [Arg.String (fun s -> mode:="-dot"; input1:=s); Arg.Set_string(input2)], "<spec_neg.spin> <spec.spin> : outputs a dot file");
		("-stat", Arg.Tuple [Arg.String (fun s -> mode:="-stat"; input1:=s); Arg.Set_string(input2)], "<spec_neg.spin> <spec.spin> : outputs jutst the statistics")
		] 
	in
	Arg.parse
		speclist
		(fun x -> raise (Arg.Bad ("Bad argument : " ^ x)))
		usage;

	begin match !mode with
		| "-nba2smv" ->
				let file1 = open_in !input1 in
				let ((props: GateSet.t), (i2m: int -> GateSet.t), nba) = Nba.from_spin file1 in
				print_endline (Nba.get_smv nba i2m props);
				exit 0
		| "-smv" | "-spin" | "-dot" | "-stat" -> ()
		| _ -> 
				Arg.usage speclist usage;
				exit 1
	end;


	let file1 = open_in !input1 in
	let file2 = open_in !input2 in
	(* i2m maps an integer 1,..,nS to the coresponding model *)
		
	let ((props: GateSet.t), (i2m: int -> GateSet.t), nba) = Nba.from_spin file1 in
	let (props, i2m, nba_neg) = Nba.from_spin file2 in
	
	(* let (props, i2m, gba) = Gba.parse_channel file1 in let (props, i2m,   *)
	(* gba_neg) = Gba.parse_channel file2 in                                 *)
	
	let a2str a = (* function that maps an int letter to a string *)
		(* let m = (IntMap.find a i2m) in *)
		let m = i2m a in
		let p2str p = match p with Prop s -> s | _ -> failwith "main:a2str: not a prop" in
		GateSet.fold (fun p str -> str^p2str p) m ""
	in
	
	let (nNba, _, _, _, _) = nba in
	let (nNegNba, _, _, _, _) = nba_neg in
	
	let (wdba, wdba_neg) =
		if nNba <= nNegNba then
			let wdba = Wdba.from_nba nba a2str in
			(wdba, Wdba.negate wdba)
		else
			let wdba_neg = Wdba.from_nba nba_neg a2str in
			(Wdba.negate wdba_neg, wdba_neg)
	in
	
	let min_wdba = Wdba.minimize wdba in
	let min_wdba_neg = Wdba.negate min_wdba in
	(* wdba i2m props);                                                      *)
	
	(* Calculates the class of the specification *)
	let spec_type (nba:Nba.nba) (nba_neg:Nba.nba) (mwdba:Wdba.wdba) (mwdba_neg:Wdba.wdba) : specT =
		let autox = Nba.intersect (Nba.from_dfa wdba_neg) nba in
		let autoy = Nba.intersect (Nba.from_dfa wdba) nba_neg in
		
		if Nba.isEmpty autox && Nba.isEmpty autoy then
			if Wdba.isSafety (Wdba.mk_complete mwdba) then SAFETY else
			if Wdba.isSafety (Wdba.mk_complete mwdba_neg) then GUARANTEE else
			OBLIGATION
		else
			REGULAR	
	in
	
	(* checks whether the formula specifies an obligation property *)
	let phitype = match spec_type nba nba_neg min_wdba min_wdba_neg with
		| REGULAR -> "regular"
		| OBLIGATION -> "obligation"
		| SAFETY -> "safety"
		| GUARANTEE -> "guarantee"
	in
	if phitype = "regular" then begin
		print_endline ("Property is not WDBA-representable.");
		exit 0
	end;

	let (nWdba, _, _, _, _) = Wdba.rmRejSink wdba in
	let (nMinWdba, _, _, _, _) = Wdba.rmRejSink min_wdba in
		
		
	match !mode with
	| "-stat" ->
			print_endline ("type, BA, -BA, WDBA, minWDBA:  "^(phitype)^", "^ Std.dump nNba^", "^ Std.dump nNegNba^", "^ Std.dump nWdba^", "^ Std.dump nMinWdba)
	| "-smv" ->
			print_endline (Wdba.get_smv min_wdba i2m props);
			print_endline ("-- type, BA, -BA, WDBA, minWDBA:  "^(phitype)^", "^ Std.dump nNba^", "^ Std.dump nNegNba^", "^ Std.dump nWdba^", "^ Std.dump nMinWdba)
	| "-dot" ->
			print_endline (Wdba.get_dot min_wdba i2m props);
			print_endline ("/* type, BA, -BA, WDBA, minWDBA:  "^(phitype)^", "^ Std.dump nNba^", "^ Std.dump nNegNba^", "^ Std.dump nWdba^", "^ Std.dump nMinWdba ^" */")
	| "-spin" ->
			print_endline (Wdba.get_never_claim min_wdba i2m props);
			print_endline ("/* type, BA, -BA, WDBA, minWDBA:  "^(phitype)^", "^ Std.dump nNba^", "^ Std.dump nNegNba^", "^ Std.dump nWdba^", "^ Std.dump nMinWdba ^" */")
	| _ -> 
			Arg.usage speclist usage


